Process: Node 1(1)(1)

We start with a table that describes for each variable of this process, what type it has and what range of values have been observed. Possible types are integer, double and string. A range of values is provided only for variables of type integer or double. If a variable changes in value, the table gives the position of the two events that perform the first and last change in value. If no remarks are given, then the variable is properly initialized, it gets assigned a value by some action at least once and its values do not show a monotonic behavior (in case of numerical values).

Name(Identifier)TypeRange1st change at eventlast change at eventRemarks
State of node 1(node1_state)int = 1 Variable is constant!
Number of packets dropped by node 1(node1_dropped)int = 0 Variable is constant!
Number of packets received by node 1(node1_received)int in {0,...,73}13997 Variable is monotonously non-decreasing!
Number of packets sent by node 1(node1_sent)int in {0,...,73}161000 Variable is monotonously non-decreasing!

The following graph shows the progress measure of the sequence, which is the length of the trace if cycles are removed:
Sorry, figure for the caption is missing